COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00010 00003	.skip 1
C00011 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.cb DESCRIBING RECURSIVE FUNCTIONS IN FIRST ORDER LOGIC

	After all these years, it turns out that first order logic
is adequate for directly representing Lisp-like recursive function
definitions.  Most of the idea is present in (Cartwright 1976),
from which I learned it,
though it may have been anticipated by others.  Moreover,
some of the methods of proving assertions about such
functions, e.g. subgoal induction and the inductive assertion
method can be expressed as axiom schemata.  Another useful idea
may be that of higher order axiom schemata in first order logic.

	We start with the Lisp ⊗append function.  The usual internal
notation for its definition is

!!a0:	(DE APPEND (U V) (COND ((NULL U) V) (T (CONS (CAR U) (APPEND (CDR U) V))))),

but we shall write it

!!a1:	%2u * v ← qif qn u qthen v qelse qa u . [qd u * v]%1,

using the infix * for ⊗append and the other conventions of a proposed
(McCarthy 1977)
Lisp publication language.

	When we write such a recursive function definition, we
need not know for what values of its arguments the computation
terminates.  We shall take the ← symbol as meaning that we
want the least fixed point of the corresponding functional equation.
To emphasize the point,

!!a2:	%2f x ← f x%1

and

!!a3:	%2f x ← 1 + f x%1

are considered perfectly good recursive function definitions, both
yielding the totally undefined partial function.  (Note our convention
that parentheses can be omitted for functions and predicates of one
argument).  The former has every partial function as a solution of
the functional equation and the second has only the totally undefined
function.

	Nevertheless, Cartwright showed that we can rewrite a
recursive function definition by a sentence of first order logic
provided the functions are given suitable interpretation.
In the case of ⊗append, we get

!!a4:	%2∀u v.(u * v = qif qn u qthen v qelse qa u . [qd u * v]%1,

and ({eq a3}) becomes

!!a5:	%2∀x.(f x = 1 + f x)%1.

	The equations are interpreted as follows: The domain of
interest, the Lisp lists or the integers in the above cases,
is considered as imbedded in a larger domain.  The larger domain
does not need to be specified, but you may imagine it to contain
only one element besides those in the lower domain - the undefined
element %AW%1.  There is no need to say what elements it contains,
because the proofs don't depend on it.  The quantifiers
using lower case letters are over the inner domain - Lisp lists
or integers.  However, the values of the recursively defined functions
are not %2a priori%1 considered to be in the inner domain.  In the case
of ⊗append, it will be proved from suitable Lisp axioms that %2u * v%1
is a list, and it follows from suitable integer axioms
that ⊗g(x) is never an integer.

What allows us to write the equations is the interpretation that
the equation can be satisfied by the least fixed point taken in the
Scott sense.  Thus ⊗append can be taken to be the least fixed point
of the second order functional

!!a6:	%2F = λf.λu v.[qif qn u qthen v qelse qa u . f[qd u, v]]%1.

According to the Scott theory, the fixed point will indeed satisfy
({eq a4}).

	In order to prove a function total, we prove by induction
that its value is in the inner domain.  Thus, Appendix I contains
a set of axioms for Lisp and a proof that %2u * v%1 is a list.

	Cartwright used this characterization of recursive functions
to prove facts about them in his human aided first order theorem
prover.  His thesis is also based on a method of recursively defining
data structures which he calls %2typed Lisp%1.  In this note, however,
we are interested in pursuing the methods of description, and this is
as far as Cartwright takes us.

	When a function can be proved total, its functional equation
is sufficient to characterize it, because the functional equation
then has a unique solution.  However, when the function is not total,
the functional equation may have many functions as solutions, and we
need another way of characterizing the least solution that corresponds
to the computation procedure.  We ⊗attempt this by the axiom schema
.begin nofill

!!a6:	%2∀x.[islist[qif qn u qthen v qelse qa u . %Af%2[qd u, v]] ⊃
∂(25)%Af%2[u,v] = qif qn u qthen v qelse qa u . %Af%2[qd u, v]]
∂(15)⊃ ∀x.[islist[u * v] ⊃ u * v = %Af%2[u,v]]%1.

.end
Here %Af%1 is a function variable for which we may substitute any
function expression.  Once we have substituted a function expression,
we then have a sentence of first order logic, so that the schema
gives rise to an infinite collection of axioms like the axiom schema
of induction.  Note, however, that the axiom schema of induction
is of general utility, while we need a separate axiom schema for
each recursive function definition.
If we use Scott's notation, we can write the schema more compactly
as

!!a7:	%Af %8d %2F(%Af%2) ⊃ %Af %8d %2Y(F)%1,

but then it is no longer a sentence of first order logic.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of

PUBbed at {time} on {date}.%1